index.md (2421B)
1 +++ 2 title = 'Functional completeness' 3 +++ 4 # Functional completeness 5 functionally complete — every truth table can be represented by a propositional formula (and vice versa) 6 7  8 9 ## Disjunctive normal form (DNF) 10 11 this results in a disjunctive normal form (DNF, terms combined with disjunctions) 12 13 a DNF is a clause (disjunction of literals) 14 15 a DNF is of the form: 16 17 Ψ1 ∨ Ψ2 ∨ … ∨ Ψn 18 19 where Ψi is conjunctions of literals (p, ¬p, etc.) 20 21 a single letter is also a DNF 22 23 ## Conjunctive normal form (CNF) 24 25 a conjunctive normal form (CNF) is conjunction Ψ1 ∧ Ψ2 ∧ … ∧ Ψn where Ψi are disjunctions of literals 26 27 disjunctions of literals are clauses (DNF), a CNF is a conjunction of clauses 28 29  30 31 Transform any ϕ to CNF using algorithm in three easy steps 32 1. IMPL-FREE: eliminate implications 33 > ϕ ➝ Ψ ≡ ¬ ϕ ∨ Ψ 34 35 1. NNF: bring occurrences of ¬ inside, until directly in front of variable (removing double nots) 36 37 > ¬ (ϕ ∧ Ψ) ≡ ¬ ϕ ∨ ¬ Ψ 38 > ¬ (ϕ ∨ Ψ) ≡ ¬ ϕ ∧ ¬ Ψ 39 > ¬ ¬ ϕ ≡ ϕ 40 1. DISTR: use distributivity law to rearrange conj/disj 41 > ϕ ∨ (Ψ ∧ Χ) ≡ (ϕ ∨ Ψ) ∧ (ϕ ∨ Χ) 42 > (ϕ ∧ Ψ) ∨ Χ ≡ (ϕ ∨ Χ) ∧ (Ψ ∨ Χ) 43 44 Is a CNF Ψ1 ∧ Ψ2 ∧ … ∧ Ψn a tautology? 45 46 Yes, only if in each of clauses Ψi it contains literals p and ¬p for some variable p. 47 48 ## Satisfiability problem 49 given a propositional formula ϕ, find a valuation that applied to ϕ yields ⊤. 50 51 NP-complete — no efficient solution has been found 52 53 DPLL (Davis-Putnam-Logemann-Loveland) procedure: 54 checks satisfiability of formula ϕ in CNF. 55 56 ⊤ — constant true 57 58 ⊥ — constant false 59 60 applies reduction rules: 61  62 63 To check satisfiability of CNF ϕ: 64 1. Eliminate “unit” clauses 65 66 - for clause p of ϕ, replace p in ϕ by ⊤ 67 - for clause ¬ p of ϕ, replace p in ϕ by ⊥ 68 69 2. Eliminate “pure” propositional variables 70 71 - if p only occurs positively in ϕ, replace all p in ϕ by ⊤ 72 - if p only occurs negatively in ϕ, replace all p in ϕ by ⊥ 73 74 3. If ϕ is ⊤, it is satisfiable 75 4. If ϕ is ⊥, it is unsatisfiable 76 5. Choose a p in ϕ: 77 78 - replace all p in ϕ by ⊤, apply DPLL 79 - if outcome is “unsatisfiable, replace all p in ϕ by ⊥ and apply DPLL again